0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 88 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 12 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 56 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 2 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
averageA_in_gag(0, 0, 0) → averageA_out_gag(0, 0, 0)
averageA_in_gag(0, s(0), 0) → averageA_out_gag(0, s(0), 0)
averageA_in_gag(0, s(s(0)), s(0)) → averageA_out_gag(0, s(s(0)), s(0))
averageA_in_gag(0, s(s(s(T17))), s(0)) → U1_gag(T17, averageA_in_gag(0, s(T17), 0))
averageA_in_gag(s(0), 0, 0) → averageA_out_gag(s(0), 0, 0)
averageA_in_gag(s(0), s(0), s(0)) → averageA_out_gag(s(0), s(0), s(0))
averageA_in_gag(s(s(T38)), T41, T40) → U2_gag(T38, T41, T40, averageA_in_gag(T38, s(s(T41)), T40))
averageA_in_gag(s(T54), s(s(T57)), s(T56)) → U3_gag(T54, T57, T56, averageA_in_gag(s(T54), T57, T56))
averageA_in_gag(s(T64), s(s(s(T67))), s(T66)) → U4_gag(T64, T67, T66, averageA_in_gag(s(s(T64)), T67, T66))
averageA_in_gag(T89, s(s(s(T92))), s(T91)) → U5_gag(T89, T92, T91, averageA_in_gag(T89, s(T92), T91))
averageA_in_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → U6_gag(T99, T102, T101, averageA_in_gag(s(s(T99)), T102, T101))
U6_gag(T99, T102, T101, averageA_out_gag(s(s(T99)), T102, T101)) → averageA_out_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101)))
U5_gag(T89, T92, T91, averageA_out_gag(T89, s(T92), T91)) → averageA_out_gag(T89, s(s(s(T92))), s(T91))
U4_gag(T64, T67, T66, averageA_out_gag(s(s(T64)), T67, T66)) → averageA_out_gag(s(T64), s(s(s(T67))), s(T66))
U3_gag(T54, T57, T56, averageA_out_gag(s(T54), T57, T56)) → averageA_out_gag(s(T54), s(s(T57)), s(T56))
U2_gag(T38, T41, T40, averageA_out_gag(T38, s(s(T41)), T40)) → averageA_out_gag(s(s(T38)), T41, T40)
U1_gag(T17, averageA_out_gag(0, s(T17), 0)) → averageA_out_gag(0, s(s(s(T17))), s(0))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
averageA_in_gag(0, 0, 0) → averageA_out_gag(0, 0, 0)
averageA_in_gag(0, s(0), 0) → averageA_out_gag(0, s(0), 0)
averageA_in_gag(0, s(s(0)), s(0)) → averageA_out_gag(0, s(s(0)), s(0))
averageA_in_gag(0, s(s(s(T17))), s(0)) → U1_gag(T17, averageA_in_gag(0, s(T17), 0))
averageA_in_gag(s(0), 0, 0) → averageA_out_gag(s(0), 0, 0)
averageA_in_gag(s(0), s(0), s(0)) → averageA_out_gag(s(0), s(0), s(0))
averageA_in_gag(s(s(T38)), T41, T40) → U2_gag(T38, T41, T40, averageA_in_gag(T38, s(s(T41)), T40))
averageA_in_gag(s(T54), s(s(T57)), s(T56)) → U3_gag(T54, T57, T56, averageA_in_gag(s(T54), T57, T56))
averageA_in_gag(s(T64), s(s(s(T67))), s(T66)) → U4_gag(T64, T67, T66, averageA_in_gag(s(s(T64)), T67, T66))
averageA_in_gag(T89, s(s(s(T92))), s(T91)) → U5_gag(T89, T92, T91, averageA_in_gag(T89, s(T92), T91))
averageA_in_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → U6_gag(T99, T102, T101, averageA_in_gag(s(s(T99)), T102, T101))
U6_gag(T99, T102, T101, averageA_out_gag(s(s(T99)), T102, T101)) → averageA_out_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101)))
U5_gag(T89, T92, T91, averageA_out_gag(T89, s(T92), T91)) → averageA_out_gag(T89, s(s(s(T92))), s(T91))
U4_gag(T64, T67, T66, averageA_out_gag(s(s(T64)), T67, T66)) → averageA_out_gag(s(T64), s(s(s(T67))), s(T66))
U3_gag(T54, T57, T56, averageA_out_gag(s(T54), T57, T56)) → averageA_out_gag(s(T54), s(s(T57)), s(T56))
U2_gag(T38, T41, T40, averageA_out_gag(T38, s(s(T41)), T40)) → averageA_out_gag(s(s(T38)), T41, T40)
U1_gag(T17, averageA_out_gag(0, s(T17), 0)) → averageA_out_gag(0, s(s(s(T17))), s(0))
AVERAGEA_IN_GAG(0, s(s(s(T17))), s(0)) → U1_GAG(T17, averageA_in_gag(0, s(T17), 0))
AVERAGEA_IN_GAG(0, s(s(s(T17))), s(0)) → AVERAGEA_IN_GAG(0, s(T17), 0)
AVERAGEA_IN_GAG(s(s(T38)), T41, T40) → U2_GAG(T38, T41, T40, averageA_in_gag(T38, s(s(T41)), T40))
AVERAGEA_IN_GAG(s(s(T38)), T41, T40) → AVERAGEA_IN_GAG(T38, s(s(T41)), T40)
AVERAGEA_IN_GAG(s(T54), s(s(T57)), s(T56)) → U3_GAG(T54, T57, T56, averageA_in_gag(s(T54), T57, T56))
AVERAGEA_IN_GAG(s(T54), s(s(T57)), s(T56)) → AVERAGEA_IN_GAG(s(T54), T57, T56)
AVERAGEA_IN_GAG(s(T64), s(s(s(T67))), s(T66)) → U4_GAG(T64, T67, T66, averageA_in_gag(s(s(T64)), T67, T66))
AVERAGEA_IN_GAG(s(T64), s(s(s(T67))), s(T66)) → AVERAGEA_IN_GAG(s(s(T64)), T67, T66)
AVERAGEA_IN_GAG(T89, s(s(s(T92))), s(T91)) → U5_GAG(T89, T92, T91, averageA_in_gag(T89, s(T92), T91))
AVERAGEA_IN_GAG(T89, s(s(s(T92))), s(T91)) → AVERAGEA_IN_GAG(T89, s(T92), T91)
AVERAGEA_IN_GAG(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → U6_GAG(T99, T102, T101, averageA_in_gag(s(s(T99)), T102, T101))
AVERAGEA_IN_GAG(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → AVERAGEA_IN_GAG(s(s(T99)), T102, T101)
averageA_in_gag(0, 0, 0) → averageA_out_gag(0, 0, 0)
averageA_in_gag(0, s(0), 0) → averageA_out_gag(0, s(0), 0)
averageA_in_gag(0, s(s(0)), s(0)) → averageA_out_gag(0, s(s(0)), s(0))
averageA_in_gag(0, s(s(s(T17))), s(0)) → U1_gag(T17, averageA_in_gag(0, s(T17), 0))
averageA_in_gag(s(0), 0, 0) → averageA_out_gag(s(0), 0, 0)
averageA_in_gag(s(0), s(0), s(0)) → averageA_out_gag(s(0), s(0), s(0))
averageA_in_gag(s(s(T38)), T41, T40) → U2_gag(T38, T41, T40, averageA_in_gag(T38, s(s(T41)), T40))
averageA_in_gag(s(T54), s(s(T57)), s(T56)) → U3_gag(T54, T57, T56, averageA_in_gag(s(T54), T57, T56))
averageA_in_gag(s(T64), s(s(s(T67))), s(T66)) → U4_gag(T64, T67, T66, averageA_in_gag(s(s(T64)), T67, T66))
averageA_in_gag(T89, s(s(s(T92))), s(T91)) → U5_gag(T89, T92, T91, averageA_in_gag(T89, s(T92), T91))
averageA_in_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → U6_gag(T99, T102, T101, averageA_in_gag(s(s(T99)), T102, T101))
U6_gag(T99, T102, T101, averageA_out_gag(s(s(T99)), T102, T101)) → averageA_out_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101)))
U5_gag(T89, T92, T91, averageA_out_gag(T89, s(T92), T91)) → averageA_out_gag(T89, s(s(s(T92))), s(T91))
U4_gag(T64, T67, T66, averageA_out_gag(s(s(T64)), T67, T66)) → averageA_out_gag(s(T64), s(s(s(T67))), s(T66))
U3_gag(T54, T57, T56, averageA_out_gag(s(T54), T57, T56)) → averageA_out_gag(s(T54), s(s(T57)), s(T56))
U2_gag(T38, T41, T40, averageA_out_gag(T38, s(s(T41)), T40)) → averageA_out_gag(s(s(T38)), T41, T40)
U1_gag(T17, averageA_out_gag(0, s(T17), 0)) → averageA_out_gag(0, s(s(s(T17))), s(0))
AVERAGEA_IN_GAG(0, s(s(s(T17))), s(0)) → U1_GAG(T17, averageA_in_gag(0, s(T17), 0))
AVERAGEA_IN_GAG(0, s(s(s(T17))), s(0)) → AVERAGEA_IN_GAG(0, s(T17), 0)
AVERAGEA_IN_GAG(s(s(T38)), T41, T40) → U2_GAG(T38, T41, T40, averageA_in_gag(T38, s(s(T41)), T40))
AVERAGEA_IN_GAG(s(s(T38)), T41, T40) → AVERAGEA_IN_GAG(T38, s(s(T41)), T40)
AVERAGEA_IN_GAG(s(T54), s(s(T57)), s(T56)) → U3_GAG(T54, T57, T56, averageA_in_gag(s(T54), T57, T56))
AVERAGEA_IN_GAG(s(T54), s(s(T57)), s(T56)) → AVERAGEA_IN_GAG(s(T54), T57, T56)
AVERAGEA_IN_GAG(s(T64), s(s(s(T67))), s(T66)) → U4_GAG(T64, T67, T66, averageA_in_gag(s(s(T64)), T67, T66))
AVERAGEA_IN_GAG(s(T64), s(s(s(T67))), s(T66)) → AVERAGEA_IN_GAG(s(s(T64)), T67, T66)
AVERAGEA_IN_GAG(T89, s(s(s(T92))), s(T91)) → U5_GAG(T89, T92, T91, averageA_in_gag(T89, s(T92), T91))
AVERAGEA_IN_GAG(T89, s(s(s(T92))), s(T91)) → AVERAGEA_IN_GAG(T89, s(T92), T91)
AVERAGEA_IN_GAG(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → U6_GAG(T99, T102, T101, averageA_in_gag(s(s(T99)), T102, T101))
AVERAGEA_IN_GAG(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → AVERAGEA_IN_GAG(s(s(T99)), T102, T101)
averageA_in_gag(0, 0, 0) → averageA_out_gag(0, 0, 0)
averageA_in_gag(0, s(0), 0) → averageA_out_gag(0, s(0), 0)
averageA_in_gag(0, s(s(0)), s(0)) → averageA_out_gag(0, s(s(0)), s(0))
averageA_in_gag(0, s(s(s(T17))), s(0)) → U1_gag(T17, averageA_in_gag(0, s(T17), 0))
averageA_in_gag(s(0), 0, 0) → averageA_out_gag(s(0), 0, 0)
averageA_in_gag(s(0), s(0), s(0)) → averageA_out_gag(s(0), s(0), s(0))
averageA_in_gag(s(s(T38)), T41, T40) → U2_gag(T38, T41, T40, averageA_in_gag(T38, s(s(T41)), T40))
averageA_in_gag(s(T54), s(s(T57)), s(T56)) → U3_gag(T54, T57, T56, averageA_in_gag(s(T54), T57, T56))
averageA_in_gag(s(T64), s(s(s(T67))), s(T66)) → U4_gag(T64, T67, T66, averageA_in_gag(s(s(T64)), T67, T66))
averageA_in_gag(T89, s(s(s(T92))), s(T91)) → U5_gag(T89, T92, T91, averageA_in_gag(T89, s(T92), T91))
averageA_in_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → U6_gag(T99, T102, T101, averageA_in_gag(s(s(T99)), T102, T101))
U6_gag(T99, T102, T101, averageA_out_gag(s(s(T99)), T102, T101)) → averageA_out_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101)))
U5_gag(T89, T92, T91, averageA_out_gag(T89, s(T92), T91)) → averageA_out_gag(T89, s(s(s(T92))), s(T91))
U4_gag(T64, T67, T66, averageA_out_gag(s(s(T64)), T67, T66)) → averageA_out_gag(s(T64), s(s(s(T67))), s(T66))
U3_gag(T54, T57, T56, averageA_out_gag(s(T54), T57, T56)) → averageA_out_gag(s(T54), s(s(T57)), s(T56))
U2_gag(T38, T41, T40, averageA_out_gag(T38, s(s(T41)), T40)) → averageA_out_gag(s(s(T38)), T41, T40)
U1_gag(T17, averageA_out_gag(0, s(T17), 0)) → averageA_out_gag(0, s(s(s(T17))), s(0))
AVERAGEA_IN_GAG(s(T54), s(s(T57)), s(T56)) → AVERAGEA_IN_GAG(s(T54), T57, T56)
AVERAGEA_IN_GAG(s(s(T38)), T41, T40) → AVERAGEA_IN_GAG(T38, s(s(T41)), T40)
AVERAGEA_IN_GAG(s(T64), s(s(s(T67))), s(T66)) → AVERAGEA_IN_GAG(s(s(T64)), T67, T66)
AVERAGEA_IN_GAG(T89, s(s(s(T92))), s(T91)) → AVERAGEA_IN_GAG(T89, s(T92), T91)
AVERAGEA_IN_GAG(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → AVERAGEA_IN_GAG(s(s(T99)), T102, T101)
averageA_in_gag(0, 0, 0) → averageA_out_gag(0, 0, 0)
averageA_in_gag(0, s(0), 0) → averageA_out_gag(0, s(0), 0)
averageA_in_gag(0, s(s(0)), s(0)) → averageA_out_gag(0, s(s(0)), s(0))
averageA_in_gag(0, s(s(s(T17))), s(0)) → U1_gag(T17, averageA_in_gag(0, s(T17), 0))
averageA_in_gag(s(0), 0, 0) → averageA_out_gag(s(0), 0, 0)
averageA_in_gag(s(0), s(0), s(0)) → averageA_out_gag(s(0), s(0), s(0))
averageA_in_gag(s(s(T38)), T41, T40) → U2_gag(T38, T41, T40, averageA_in_gag(T38, s(s(T41)), T40))
averageA_in_gag(s(T54), s(s(T57)), s(T56)) → U3_gag(T54, T57, T56, averageA_in_gag(s(T54), T57, T56))
averageA_in_gag(s(T64), s(s(s(T67))), s(T66)) → U4_gag(T64, T67, T66, averageA_in_gag(s(s(T64)), T67, T66))
averageA_in_gag(T89, s(s(s(T92))), s(T91)) → U5_gag(T89, T92, T91, averageA_in_gag(T89, s(T92), T91))
averageA_in_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → U6_gag(T99, T102, T101, averageA_in_gag(s(s(T99)), T102, T101))
U6_gag(T99, T102, T101, averageA_out_gag(s(s(T99)), T102, T101)) → averageA_out_gag(T99, s(s(s(s(s(s(T102)))))), s(s(T101)))
U5_gag(T89, T92, T91, averageA_out_gag(T89, s(T92), T91)) → averageA_out_gag(T89, s(s(s(T92))), s(T91))
U4_gag(T64, T67, T66, averageA_out_gag(s(s(T64)), T67, T66)) → averageA_out_gag(s(T64), s(s(s(T67))), s(T66))
U3_gag(T54, T57, T56, averageA_out_gag(s(T54), T57, T56)) → averageA_out_gag(s(T54), s(s(T57)), s(T56))
U2_gag(T38, T41, T40, averageA_out_gag(T38, s(s(T41)), T40)) → averageA_out_gag(s(s(T38)), T41, T40)
U1_gag(T17, averageA_out_gag(0, s(T17), 0)) → averageA_out_gag(0, s(s(s(T17))), s(0))
AVERAGEA_IN_GAG(s(T54), s(s(T57)), s(T56)) → AVERAGEA_IN_GAG(s(T54), T57, T56)
AVERAGEA_IN_GAG(s(s(T38)), T41, T40) → AVERAGEA_IN_GAG(T38, s(s(T41)), T40)
AVERAGEA_IN_GAG(s(T64), s(s(s(T67))), s(T66)) → AVERAGEA_IN_GAG(s(s(T64)), T67, T66)
AVERAGEA_IN_GAG(T89, s(s(s(T92))), s(T91)) → AVERAGEA_IN_GAG(T89, s(T92), T91)
AVERAGEA_IN_GAG(T99, s(s(s(s(s(s(T102)))))), s(s(T101))) → AVERAGEA_IN_GAG(s(s(T99)), T102, T101)
AVERAGEA_IN_GAG(s(T54), s(T56)) → AVERAGEA_IN_GAG(s(T54), T56)
AVERAGEA_IN_GAG(s(s(T38)), T40) → AVERAGEA_IN_GAG(T38, T40)
AVERAGEA_IN_GAG(s(T64), s(T66)) → AVERAGEA_IN_GAG(s(s(T64)), T66)
AVERAGEA_IN_GAG(T89, s(T91)) → AVERAGEA_IN_GAG(T89, T91)
AVERAGEA_IN_GAG(T99, s(s(T101))) → AVERAGEA_IN_GAG(s(s(T99)), T101)
From the DPs we obtained the following set of size-change graphs: